Nuprl Definition : case_node
4,23
postcript
pdf
Case
x
;
y
=>
body
(
x
;
y
)
cont
(
x1
,
z
)
== Case
x1
of inl(
_
)
cont
(
z
,
z
) ; inr(
x2
)
x2
/
x3
,
x2@0
.
body
(
x3
;
x2@0
)
latex
Definitions
Case
x
;
y
=>
body
(
x
;
y
)
cont
FDL editor aliases
case_node
origin
cont(z,z) ; inr(x2) x2/x3,x2@0. body(x3;x2@0) cont(z,z) ; inr(x2) x2/x3,x2@0. body(x3;x2@0)